Termination of the given ITRSProblem could not be shown:



↳ ITRS
  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

del(x, nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
if2(FALSE, x, y, xs) → cons(y, del(x, xs))
max(cons(x, cons(y, xs))) → if1(>=@z(x, y), x, y, xs)
del(x, cons(y, xs)) → if2(=@z(x, y), x, y, xs)
max(cons(x, nil)) → x
if1(TRUE, x, y, xs) → max(cons(x, xs))
if2(TRUE, x, y, xs) → xs
if1(FALSE, x, y, xs) → max(cons(y, xs))
max(nil) → 0@z
sort(nil) → nil

The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


Added dependency pairs

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

del(x, nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
if2(FALSE, x, y, xs) → cons(y, del(x, xs))
max(cons(x, cons(y, xs))) → if1(>=@z(x, y), x, y, xs)
del(x, cons(y, xs)) → if2(=@z(x, y), x, y, xs)
max(cons(x, nil)) → x
if1(TRUE, x, y, xs) → max(cons(x, xs))
if2(TRUE, x, y, xs) → xs
if1(FALSE, x, y, xs) → max(cons(y, xs))
max(nil) → 0@z
sort(nil) → nil

The integer pair graph contains the following rules and edges:

(0): IF2(FALSE, x[0], y[0], xs[0]) → DEL(x[0], xs[0])
(1): SORT(cons(x[1], xs[1])) → SORT(del(max(cons(x[1], xs[1])), cons(x[1], xs[1])))
(2): IF1(TRUE, x[2], y[2], xs[2]) → MAX(cons(x[2], xs[2]))
(3): DEL(x[3], cons(y[3], xs[3])) → IF2(=@z(x[3], y[3]), x[3], y[3], xs[3])
(4): SORT(cons(x[4], xs[4])) → MAX(cons(x[4], xs[4]))
(5): SORT(cons(x[5], xs[5])) → DEL(max(cons(x[5], xs[5])), cons(x[5], xs[5]))
(6): IF1(FALSE, x[6], y[6], xs[6]) → MAX(cons(y[6], xs[6]))
(7): MAX(cons(x[7], cons(y[7], xs[7]))) → IF1(>=@z(x[7], y[7]), x[7], y[7], xs[7])

(0) -> (3), if ((xs[0] →* cons(y[3], xs[3]))∧(x[0] →* x[3]))


(1) -> (1), if ((del(max(cons(x[1], xs[1])), cons(x[1], xs[1])) →* cons(x[1]a, xs[1]a)))


(1) -> (4), if ((del(max(cons(x[1], xs[1])), cons(x[1], xs[1])) →* cons(x[4], xs[4])))


(1) -> (5), if ((del(max(cons(x[1], xs[1])), cons(x[1], xs[1])) →* cons(x[5], xs[5])))


(2) -> (7), if ((xs[2] →* cons(y[7], xs[7]))∧(x[2] →* x[7]))


(3) -> (0), if ((xs[3] →* xs[0])∧(x[3] →* x[0])∧(y[3] →* y[0])∧(=@z(x[3], y[3]) →* FALSE))


(4) -> (7), if ((xs[4] →* cons(y[7], xs[7]))∧(x[4] →* x[7]))


(5) -> (3), if ((xs[5] →* xs[3])∧(x[5] →* y[3])∧(max(cons(x[5], xs[5])) →* x[3]))


(6) -> (7), if ((xs[6] →* cons(y[7], xs[7]))∧(y[6] →* x[7]))


(7) -> (2), if ((xs[7] →* xs[2])∧(x[7] →* x[2])∧(y[7] →* y[2])∧(>=@z(x[7], y[7]) →* TRUE))


(7) -> (6), if ((xs[7] →* xs[6])∧(x[7] →* x[6])∧(y[7] →* y[6])∧(>=@z(x[7], y[7]) →* FALSE))



The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

del(x, nil) → nil
if2(FALSE, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(=@z(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(>=@z(x, y), x, y, xs)
if1(FALSE, x, y, xs) → max(cons(y, xs))
if1(TRUE, x, y, xs) → max(cons(x, xs))
if2(TRUE, x, y, xs) → xs

The integer pair graph contains the following rules and edges:

(0): IF2(FALSE, x[0], y[0], xs[0]) → DEL(x[0], xs[0])
(1): SORT(cons(x[1], xs[1])) → SORT(del(max(cons(x[1], xs[1])), cons(x[1], xs[1])))
(2): IF1(TRUE, x[2], y[2], xs[2]) → MAX(cons(x[2], xs[2]))
(3): DEL(x[3], cons(y[3], xs[3])) → IF2(=@z(x[3], y[3]), x[3], y[3], xs[3])
(4): SORT(cons(x[4], xs[4])) → MAX(cons(x[4], xs[4]))
(5): SORT(cons(x[5], xs[5])) → DEL(max(cons(x[5], xs[5])), cons(x[5], xs[5]))
(6): IF1(FALSE, x[6], y[6], xs[6]) → MAX(cons(y[6], xs[6]))
(7): MAX(cons(x[7], cons(y[7], xs[7]))) → IF1(>=@z(x[7], y[7]), x[7], y[7], xs[7])

(0) -> (3), if ((xs[0] →* cons(y[3], xs[3]))∧(x[0] →* x[3]))


(1) -> (1), if ((del(max(cons(x[1], xs[1])), cons(x[1], xs[1])) →* cons(x[1]a, xs[1]a)))


(1) -> (4), if ((del(max(cons(x[1], xs[1])), cons(x[1], xs[1])) →* cons(x[4], xs[4])))


(1) -> (5), if ((del(max(cons(x[1], xs[1])), cons(x[1], xs[1])) →* cons(x[5], xs[5])))


(2) -> (7), if ((xs[2] →* cons(y[7], xs[7]))∧(x[2] →* x[7]))


(3) -> (0), if ((xs[3] →* xs[0])∧(x[3] →* x[0])∧(y[3] →* y[0])∧(=@z(x[3], y[3]) →* FALSE))


(4) -> (7), if ((xs[4] →* cons(y[7], xs[7]))∧(x[4] →* x[7]))


(5) -> (3), if ((xs[5] →* xs[3])∧(x[5] →* y[3])∧(max(cons(x[5], xs[5])) →* x[3]))


(6) -> (7), if ((xs[6] →* cons(y[7], xs[7]))∧(y[6] →* x[7]))


(7) -> (2), if ((xs[7] →* xs[2])∧(x[7] →* x[2])∧(y[7] →* y[2])∧(>=@z(x[7], y[7]) →* TRUE))


(7) -> (6), if ((xs[7] →* xs[6])∧(x[7] →* x[6])∧(y[7] →* y[6])∧(>=@z(x[7], y[7]) →* FALSE))



The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 2 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

del(x, nil) → nil
if2(FALSE, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(=@z(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(>=@z(x, y), x, y, xs)
if1(FALSE, x, y, xs) → max(cons(y, xs))
if1(TRUE, x, y, xs) → max(cons(x, xs))
if2(TRUE, x, y, xs) → xs

The integer pair graph contains the following rules and edges:

(2): IF1(TRUE, x[2], y[2], xs[2]) → MAX(cons(x[2], xs[2]))
(7): MAX(cons(x[7], cons(y[7], xs[7]))) → IF1(>=@z(x[7], y[7]), x[7], y[7], xs[7])
(6): IF1(FALSE, x[6], y[6], xs[6]) → MAX(cons(y[6], xs[6]))

(7) -> (6), if ((xs[7] →* xs[6])∧(x[7] →* x[6])∧(y[7] →* y[6])∧(>=@z(x[7], y[7]) →* FALSE))


(7) -> (2), if ((xs[7] →* xs[2])∧(x[7] →* x[2])∧(y[7] →* y[2])∧(>=@z(x[7], y[7]) →* TRUE))


(6) -> (7), if ((xs[6] →* cons(y[7], xs[7]))∧(y[6] →* x[7]))


(2) -> (7), if ((xs[2] →* cons(y[7], xs[7]))∧(x[2] →* x[7]))



The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(2): IF1(TRUE, x[2], y[2], xs[2]) → MAX(cons(x[2], xs[2]))
(7): MAX(cons(x[7], cons(y[7], xs[7]))) → IF1(>=@z(x[7], y[7]), x[7], y[7], xs[7])
(6): IF1(FALSE, x[6], y[6], xs[6]) → MAX(cons(y[6], xs[6]))

(7) -> (6), if ((xs[7] →* xs[6])∧(x[7] →* x[6])∧(y[7] →* y[6])∧(>=@z(x[7], y[7]) →* FALSE))


(7) -> (2), if ((xs[7] →* xs[2])∧(x[7] →* x[2])∧(y[7] →* y[2])∧(>=@z(x[7], y[7]) →* TRUE))


(6) -> (7), if ((xs[6] →* cons(y[7], xs[7]))∧(y[6] →* x[7]))


(2) -> (7), if ((xs[2] →* cons(y[7], xs[7]))∧(x[2] →* x[7]))



The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair IF1(TRUE, x[2], y[2], xs[2]) → MAX(cons(x[2], xs[2])) the following chains were created:




For Pair MAX(cons(x[7], cons(y[7], xs[7]))) → IF1(>=@z(x[7], y[7]), x[7], y[7], xs[7]) the following chains were created:




For Pair IF1(FALSE, x[6], y[6], xs[6]) → MAX(cons(y[6], xs[6])) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(cons(x1, x2)) = 1 + x2   
POL(>=@z(x1, x2)) = 0   
POL(IF1(x1, x2, x3, x4)) = x4   
POL(TRUE) = 0   
POL(FALSE) = 0   
POL(MAX(x1)) = -1 + x1   
POL(undefined) = 0   

The following pairs are in P>:

MAX(cons(x[7], cons(y[7], xs[7]))) → IF1(>=@z(x[7], y[7]), x[7], y[7], xs[7])

The following pairs are in Pbound:

IF1(TRUE, x[2], y[2], xs[2]) → MAX(cons(x[2], xs[2]))
MAX(cons(x[7], cons(y[7], xs[7]))) → IF1(>=@z(x[7], y[7]), x[7], y[7], xs[7])
IF1(FALSE, x[6], y[6], xs[6]) → MAX(cons(y[6], xs[6]))

The following pairs are in P≥:

IF1(TRUE, x[2], y[2], xs[2]) → MAX(cons(x[2], xs[2]))
IF1(FALSE, x[6], y[6], xs[6]) → MAX(cons(y[6], xs[6]))

There are no usable rules.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                          ↳ IDependencyGraphProof
                        ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph is empty.
The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                        ↳ IDP
                          ↳ IDependencyGraphProof
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph contains the following rules and edges:

(2): IF1(TRUE, x[2], y[2], xs[2]) → MAX(cons(x[2], xs[2]))
(6): IF1(FALSE, x[6], y[6], xs[6]) → MAX(cons(y[6], xs[6]))


The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

del(x, nil) → nil
if2(FALSE, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(=@z(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(>=@z(x, y), x, y, xs)
if1(FALSE, x, y, xs) → max(cons(y, xs))
if1(TRUE, x, y, xs) → max(cons(x, xs))
if2(TRUE, x, y, xs) → xs

The integer pair graph contains the following rules and edges:

(3): DEL(x[3], cons(y[3], xs[3])) → IF2(=@z(x[3], y[3]), x[3], y[3], xs[3])
(0): IF2(FALSE, x[0], y[0], xs[0]) → DEL(x[0], xs[0])

(0) -> (3), if ((xs[0] →* cons(y[3], xs[3]))∧(x[0] →* x[3]))


(3) -> (0), if ((xs[3] →* xs[0])∧(x[3] →* x[0])∧(y[3] →* y[0])∧(=@z(x[3], y[3]) →* FALSE))



The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(3): DEL(x[3], cons(y[3], xs[3])) → IF2(=@z(x[3], y[3]), x[3], y[3], xs[3])
(0): IF2(FALSE, x[0], y[0], xs[0]) → DEL(x[0], xs[0])

(0) -> (3), if ((xs[0] →* cons(y[3], xs[3]))∧(x[0] →* x[3]))


(3) -> (0), if ((xs[3] →* xs[0])∧(x[3] →* x[0])∧(y[3] →* y[0])∧(=@z(x[3], y[3]) →* FALSE))



The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair DEL(x[3], cons(y[3], xs[3])) → IF2(=@z(x[3], y[3]), x[3], y[3], xs[3]) the following chains were created:




For Pair IF2(FALSE, x[0], y[0], xs[0]) → DEL(x[0], xs[0]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(cons(x1, x2)) = 1 + x2   
POL(=@z(x1, x2)) = 0   
POL(IF2(x1, x2, x3, x4)) = -1 + (2)x4 + (-1)x2   
POL(TRUE) = 0   
POL(DEL(x1, x2)) = -1 + (2)x2 + (-1)x1   
POL(FALSE) = 0   
POL(undefined) = 0   

The following pairs are in P>:

DEL(x[3], cons(y[3], xs[3])) → IF2(=@z(x[3], y[3]), x[3], y[3], xs[3])

The following pairs are in Pbound:

DEL(x[3], cons(y[3], xs[3])) → IF2(=@z(x[3], y[3]), x[3], y[3], xs[3])
IF2(FALSE, x[0], y[0], xs[0]) → DEL(x[0], xs[0])

The following pairs are in P≥:

IF2(FALSE, x[0], y[0], xs[0]) → DEL(x[0], xs[0])

There are no usable rules.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                          ↳ IDependencyGraphProof
                        ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph is empty.
The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                        ↳ IDP
                          ↳ IDependencyGraphProof
              ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph contains the following rules and edges:

(0): IF2(FALSE, x[0], y[0], xs[0]) → DEL(x[0], xs[0])


The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ IDPtoQDPProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

del(x, nil) → nil
if2(FALSE, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(=@z(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(>=@z(x, y), x, y, xs)
if1(FALSE, x, y, xs) → max(cons(y, xs))
if1(TRUE, x, y, xs) → max(cons(x, xs))
if2(TRUE, x, y, xs) → xs

The integer pair graph contains the following rules and edges:

(1): SORT(cons(x[1], xs[1])) → SORT(del(max(cons(x[1], xs[1])), cons(x[1], xs[1])))

(1) -> (1), if ((del(max(cons(x[1], xs[1])), cons(x[1], xs[1])) →* cons(x[1]a, xs[1]a)))



The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(FALSE, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(TRUE, x0, x1, x2)
if2(TRUE, x0, x1, x2)
if1(FALSE, x0, x1, x2)
max(nil)
sort(nil)


Represented integers and predefined function symbols by Terms

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ IDPtoQDPProof
                  ↳ QDP
                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x[1], xs[1])) → SORT(del(max(cons(x[1], xs[1])), cons(x[1], xs[1])))

The TRS R consists of the following rules:

del(x, nil) → nil
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(equal_int(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(greatereq_int(x, y), x, y, xs)
if1(false, x, y, xs) → max(cons(y, xs))
if1(true, x, y, xs) → max(cons(x, xs))
if2(true, x, y, xs) → xs
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

del(x0, nil)
sort(cons(x0, x1))
if2(false, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(true, x0, x1, x2)
if2(true, x0, x1, x2)
if1(false, x0, x1, x2)
max(nil)
sort(nil)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

sort(cons(x0, x1))
sort(nil)



↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ IDPtoQDPProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x[1], xs[1])) → SORT(del(max(cons(x[1], xs[1])), cons(x[1], xs[1])))

The TRS R consists of the following rules:

del(x, nil) → nil
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(equal_int(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(greatereq_int(x, y), x, y, xs)
if1(false, x, y, xs) → max(cons(y, xs))
if1(true, x, y, xs) → max(cons(x, xs))
if2(true, x, y, xs) → xs
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

del(x0, nil)
if2(false, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(true, x0, x1, x2)
if2(true, x0, x1, x2)
if1(false, x0, x1, x2)
max(nil)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule SORT(cons(x[1], xs[1])) → SORT(del(max(cons(x[1], xs[1])), cons(x[1], xs[1]))) at position [0] we obtained the following new rules [LPAR04]:

SORT(cons(x[1], xs[1])) → SORT(if2(equal_int(max(cons(x[1], xs[1])), x[1]), max(cons(x[1], xs[1])), x[1], xs[1]))



↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ IDPtoQDPProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x[1], xs[1])) → SORT(if2(equal_int(max(cons(x[1], xs[1])), x[1]), max(cons(x[1], xs[1])), x[1], xs[1]))

The TRS R consists of the following rules:

del(x, nil) → nil
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(equal_int(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(greatereq_int(x, y), x, y, xs)
if1(false, x, y, xs) → max(cons(y, xs))
if1(true, x, y, xs) → max(cons(x, xs))
if2(true, x, y, xs) → xs
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

del(x0, nil)
if2(false, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(true, x0, x1, x2)
if2(true, x0, x1, x2)
if1(false, x0, x1, x2)
max(nil)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule SORT(cons(x[1], xs[1])) → SORT(if2(equal_int(max(cons(x[1], xs[1])), x[1]), max(cons(x[1], xs[1])), x[1], xs[1])) at position [0] we obtained the following new rules [LPAR04]:

SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(if1(greatereq_int(x0, x1), x0, x1, x2), x0), max(cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(max(cons(x0, cons(x1, x2))), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2)))
SORT(cons(x0, nil)) → SORT(if2(equal_int(x0, x0), max(cons(x0, nil)), x0, nil))
SORT(cons(x0, nil)) → SORT(if2(equal_int(max(cons(x0, nil)), x0), x0, x0, nil))



↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ IDPtoQDPProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(if1(greatereq_int(x0, x1), x0, x1, x2), x0), max(cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(max(cons(x0, cons(x1, x2))), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2)))
SORT(cons(x0, nil)) → SORT(if2(equal_int(x0, x0), max(cons(x0, nil)), x0, nil))
SORT(cons(x0, nil)) → SORT(if2(equal_int(max(cons(x0, nil)), x0), x0, x0, nil))

The TRS R consists of the following rules:

del(x, nil) → nil
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(equal_int(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(greatereq_int(x, y), x, y, xs)
if1(false, x, y, xs) → max(cons(y, xs))
if1(true, x, y, xs) → max(cons(x, xs))
if2(true, x, y, xs) → xs
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

del(x0, nil)
if2(false, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(true, x0, x1, x2)
if2(true, x0, x1, x2)
if1(false, x0, x1, x2)
max(nil)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(if1(greatereq_int(x0, x1), x0, x1, x2), x0), max(cons(x0, cons(x1, x2))), x0, cons(x1, x2))) at position [0,1] we obtained the following new rules [LPAR04]:

SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(if1(greatereq_int(x0, x1), x0, x1, x2), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2)))



↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ IDPtoQDPProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(max(cons(x0, cons(x1, x2))), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2)))
SORT(cons(x0, nil)) → SORT(if2(equal_int(x0, x0), max(cons(x0, nil)), x0, nil))
SORT(cons(x0, nil)) → SORT(if2(equal_int(max(cons(x0, nil)), x0), x0, x0, nil))
SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(if1(greatereq_int(x0, x1), x0, x1, x2), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2)))

The TRS R consists of the following rules:

del(x, nil) → nil
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(equal_int(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(greatereq_int(x, y), x, y, xs)
if1(false, x, y, xs) → max(cons(y, xs))
if1(true, x, y, xs) → max(cons(x, xs))
if2(true, x, y, xs) → xs
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

del(x0, nil)
if2(false, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(true, x0, x1, x2)
if2(true, x0, x1, x2)
if1(false, x0, x1, x2)
max(nil)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(max(cons(x0, cons(x1, x2))), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2))) at position [0,0,0] we obtained the following new rules [LPAR04]:

SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(if1(greatereq_int(x0, x1), x0, x1, x2), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2)))



↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ IDPtoQDPProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, nil)) → SORT(if2(equal_int(x0, x0), max(cons(x0, nil)), x0, nil))
SORT(cons(x0, nil)) → SORT(if2(equal_int(max(cons(x0, nil)), x0), x0, x0, nil))
SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(if1(greatereq_int(x0, x1), x0, x1, x2), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2)))

The TRS R consists of the following rules:

del(x, nil) → nil
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(equal_int(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(greatereq_int(x, y), x, y, xs)
if1(false, x, y, xs) → max(cons(y, xs))
if1(true, x, y, xs) → max(cons(x, xs))
if2(true, x, y, xs) → xs
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

del(x0, nil)
if2(false, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(true, x0, x1, x2)
if2(true, x0, x1, x2)
if1(false, x0, x1, x2)
max(nil)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule SORT(cons(x0, nil)) → SORT(if2(equal_int(x0, x0), max(cons(x0, nil)), x0, nil)) at position [0,1] we obtained the following new rules [LPAR04]:

SORT(cons(x0, nil)) → SORT(if2(equal_int(x0, x0), x0, x0, nil))



↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ IDPtoQDPProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, nil)) → SORT(if2(equal_int(max(cons(x0, nil)), x0), x0, x0, nil))
SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(if1(greatereq_int(x0, x1), x0, x1, x2), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2)))
SORT(cons(x0, nil)) → SORT(if2(equal_int(x0, x0), x0, x0, nil))

The TRS R consists of the following rules:

del(x, nil) → nil
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(equal_int(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(greatereq_int(x, y), x, y, xs)
if1(false, x, y, xs) → max(cons(y, xs))
if1(true, x, y, xs) → max(cons(x, xs))
if2(true, x, y, xs) → xs
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

del(x0, nil)
if2(false, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(true, x0, x1, x2)
if2(true, x0, x1, x2)
if1(false, x0, x1, x2)
max(nil)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule SORT(cons(x0, nil)) → SORT(if2(equal_int(max(cons(x0, nil)), x0), x0, x0, nil)) at position [0,0,0] we obtained the following new rules [LPAR04]:

SORT(cons(x0, nil)) → SORT(if2(equal_int(x0, x0), x0, x0, nil))



↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ IDPtoQDPProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, cons(x1, x2))) → SORT(if2(equal_int(if1(greatereq_int(x0, x1), x0, x1, x2), x0), if1(greatereq_int(x0, x1), x0, x1, x2), x0, cons(x1, x2)))
SORT(cons(x0, nil)) → SORT(if2(equal_int(x0, x0), x0, x0, nil))

The TRS R consists of the following rules:

del(x, nil) → nil
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if2(equal_int(x, y), x, y, xs)
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(greatereq_int(x, y), x, y, xs)
if1(false, x, y, xs) → max(cons(y, xs))
if1(true, x, y, xs) → max(cons(x, xs))
if2(true, x, y, xs) → xs
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

del(x0, nil)
if2(false, x0, x1, x2)
max(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
max(cons(x0, nil))
if1(true, x0, x1, x2)
if2(true, x0, x1, x2)
if1(false, x0, x1, x2)
max(nil)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.